<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ProofDerivationStepEntry</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ProofDerivationStepEntry";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/ProofConstants.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/SubstMapEntry.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/ProofDerivationStepEntry.html" target="_top">Frames</a></li>
<li><a href="ProofDerivationStepEntry.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.verify</div>
<h2 title="Class ProofDerivationStepEntry" class="title">Class ProofDerivationStepEntry</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.verify.ProofDerivationStepEntry</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">ProofDerivationStepEntry</span>
extends java.lang.Object</pre>
<div class="block">Proof Derivation Step Entry is a simple data structure used to hold a
 non-syntax axiom assertion proof step (i.e. a derivation step.)
 <p>
 We use mmj.verify.VerifyProofs to generate the ProofDerivationStepEntry
 objects for a theorem because VerifyProofs already has the complete mechanism
 for dealing with a Metamath proof and generating the formula resulting from
 each derivation step.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#formula">formula</a></strong></code>
<div class="block">formula is the formula resulting from the derivation using the Ref and
 its hypotheses.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#formulaParseTree">formulaParseTree</a></strong></code>
<div class="block">formulaParseTree is here for use in TMFF, Text Mode Formula Formatting.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#hypStep">hypStep</a></strong></code>
<div class="block">hypStepNbr contains the stepNbr's of previous steps that are to be used
 as hypotheses for the Ref Assrt in the current step.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#isHyp">isHyp</a></strong></code>
<div class="block">isHyp indicates if this step is one of the Theorem's logical hypothesis
 steps.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#proofLevel">proofLevel</a></strong></code>
<div class="block">Level number of the step within the proof where the qed step has level 0
 and each hypothesis is one level higher.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#refLabel">refLabel</a></strong></code>
<div class="block">refLabel is the label of the Assrt used to justify the step, and which
 creates the derivation of the step's formula.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#step">step</a></strong></code>
<div class="block">stepNbr is an integer ranging from 1 through n - 1, where 'n' is the last
 derivation step of the proof -- and the final step number is "qed".</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#ProofDerivationStepEntry()">ProofDerivationStepEntry</a></strong>()</code>&nbsp;</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#computeProofLevels(java.util.List)">computeProofLevels</a></strong>(java.util.List&lt;<a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify">ProofDerivationStepEntry</a>&gt;&nbsp;pList)</code>
<div class="block">Compute proof level numbers for a proof stored in a
 ProofDerivationStepEntry ArrayList.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#computeProofLevelsSlowly(java.util.List)">computeProofLevelsSlowly</a></strong>(java.util.List&lt;<a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify">ProofDerivationStepEntry</a>&gt;&nbsp;pList)</code>
<div class="block">Compute proof level numbers for a proof stored in a
 ProofDerivationStepEntry ArrayList.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofDerivationStepEntry.html#toString()">toString</a></strong>()</code>&nbsp;</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="isHyp">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isHyp</h4>
<pre>public&nbsp;boolean isHyp</pre>
<div class="block">isHyp indicates if this step is one of the Theorem's logical hypothesis
 steps.</div>
</li>
</ul>
<a name="step">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>step</h4>
<pre>public&nbsp;java.lang.String step</pre>
<div class="block">stepNbr is an integer ranging from 1 through n - 1, where 'n' is the last
 derivation step of the proof -- and the final step number is "qed".</div>
</li>
</ul>
<a name="hypStep">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hypStep</h4>
<pre>public&nbsp;java.lang.String[] hypStep</pre>
<div class="block">hypStepNbr contains the stepNbr's of previous steps that are to be used
 as hypotheses for the Ref Assrt in the current step. There may be 0, 1,
 ... n hyps.</div>
</li>
</ul>
<a name="refLabel">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>refLabel</h4>
<pre>public&nbsp;java.lang.String refLabel</pre>
<div class="block">refLabel is the label of the Assrt used to justify the step, and which
 creates the derivation of the step's formula.
 <p>
 refLabel is always present on hypothesis steps because a Theorem's proof
 may not refer to the hypotheses in database sequence and so there could
 be ambiguity about which step is referring to which hypothesis.</div>
</li>
</ul>
<a name="formula">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>formula</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a> formula</pre>
<div class="block">formula is the formula resulting from the derivation using the Ref and
 its hypotheses. Except for the hypothesis steps and the final step, the
 formulas are intermediate results that are not seen -- except here and in
 a Proof Assistant ProofWorksheet, which is what the
 ProofDerivationStepEntry will be used to generate.</div>
</li>
</ul>
<a name="formulaParseTree">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>formulaParseTree</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a> formulaParseTree</pre>
<div class="block">formulaParseTree is here for use in TMFF, Text Mode Formula Formatting.
 <p>
 formulaParseTree of the formula, or null if either the parse failed or
 has not yet been attempted (VerifyProofs.getProofDerivationSteps() and
 VerifyProofs.loadProofDerivStepList() will load the parse tree for the
 theorem's formula and its logical hypotheses, but the proof step parse
 trees are not available there -- so ProofWorksheet will fill in the
 missing parses.)</div>
</li>
</ul>
<a name="proofLevel">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>proofLevel</h4>
<pre>public&nbsp;int proofLevel</pre>
<div class="block">Level number of the step within the proof where the qed step has level 0
 and each hypothesis is one level higher.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ProofDerivationStepEntry()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ProofDerivationStepEntry</h4>
<pre>public&nbsp;ProofDerivationStepEntry()</pre>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="toString()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toString</h4>
<pre>public&nbsp;java.lang.String&nbsp;toString()</pre>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>toString</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
</dl>
</li>
</ul>
<a name="computeProofLevels(java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>computeProofLevels</h4>
<pre>public static&nbsp;void&nbsp;computeProofLevels(java.util.List&lt;<a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify">ProofDerivationStepEntry</a>&gt;&nbsp;pList)</pre>
<div class="block">Compute proof level numbers for a proof stored in a
 ProofDerivationStepEntry ArrayList.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>pList</code> - ProofDerivationStepEntry ArrayList</dd></dl>
</li>
</ul>
<a name="computeProofLevelsSlowly(java.util.List)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>computeProofLevelsSlowly</h4>
<pre>public static&nbsp;void&nbsp;computeProofLevelsSlowly(java.util.List&lt;<a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify">ProofDerivationStepEntry</a>&gt;&nbsp;pList)</pre>
<div class="block">Compute proof level numbers for a proof stored in a
 ProofDerivationStepEntry ArrayList.
 <p>
 This routine is coded because there may be incomplete or invalid proofs
 that the normal routine cannot handle...and yet, 99.99% of the time we
 are dealing with complete, valid proofs so it is deemed preferable to try
 to do the computation the quick way first and see what happens.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>pList</code> - ProofDerivationStepEntry ArrayList</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/ProofConstants.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/SubstMapEntry.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/ProofDerivationStepEntry.html" target="_top">Frames</a></li>
<li><a href="ProofDerivationStepEntry.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
